es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id }. e[e1,e2].True  True 

latex

Definitions	t  T, True, x:A. B(x), e  e' , Prop, P  Q, E, e[e1,e2].P(e), P  Q, b, False, A, loc(e), Id, x. t(x), P & Q, P  Q, ES
Lemmas	event system wf, alle-between2 wf, Id wf, es-loc wf, es-loc-pred, true wf, es-E wf, es-le wf